\begin{tabbing}
$\forall$$p$:FinProbSpace, $f$:($\mathbb{N}\rightarrow\mathbb{N}$), $X$:($n$:$\mathbb{N}\rightarrow$RandomVariable($p$;$f$($n$))).
\\[0ex]rv{-}iid($p$;$n$.$f$($n$);$n$.$X$($n$))
\\[0ex]$\Rightarrow$ \=($\forall$${\it mean}$:$\mathbb{Q}$.\+
\\[0ex](E($f$(0);$X$(0)) = ${\it mean}$)
\\[0ex]$\Rightarrow$ nullset($p$;$\lambda$$s$.$\exists$\=$q$:$\mathbb{Q}$\+
\\[0ex](0 $<$ $q$
\\[0ex]\& (\=$\forall$$n$:$\mathbb{N}$.\+
\\[0ex]$\exists$$m$:$\mathbb{N}$. (($n$ $<$ $m$) \& $q$ $\leq$ $\mid\Sigma$0 $\leq$ $i$ $<$ $m$. (1/$m$) $\ast$ ($X$($i$)($s$)) {-} ${\it mean}$$\mid$)))))
\-\-\-
\end{tabbing}